T:Type, eq:EqDecider(T), es:event_system{i:l}, x:Id, e:{e:es-E(es)| es-dtype(es; loc(e); x; T)} .
(x changed before e)
 e''[(last change to x before e),e).es-after(es; x; e'') = es-when(es; x; e)  T 

latex

Definitions	x:A. B(x), P  Q, e[e1,e2).P(e), t  T, prop{i:l}, T, True, es-dtype(es; i; x; T), P  Q, A c B, e(e1,e2].P(e), es-le(es; e; e'), P  Q, x:A. B(x), es-locl(es; e; e'), P  Q, SqStable(P), sq_type(T), guard(T), @e(xv)
Lemmas	last-change-property, es-locl wf, es-le wf, last-change wf, assert wf, changed wf, es-E wf, es-dtype wf, es-loc wf, Id wf, event system wf, deq wf, es-next, es-le-trans3, es-pred-locl, es-le weakening, es-after wf, es-le-loc, squash wf, true wf, es-loc-pred, es-locl-iff, es-vartype wf, es-after-pred2, sq stable from decidable, es-isconst wf, decidable assert, Id sq, sq stable subtype rel